\section{\label{sec:related}Approches to detected Races}
\label{sec:related}

\Comment{\noindent\textbf{Space reduction techniques.}~To alleviate the high
cost associated with state-space exploration program model checkers
use, often lossy, space reduction
techniques~\citep{lerda:01,visser-etal-2005,MusuvathiQadeer2007}.  The
opportunity of improvement of \tname{} is directly proportional to
such high cost.  Musuvathi and Qadeer~\citep{MusuvathiQadeer2007}
recently proposed CHESS to constrain the number of context switches
that the model checker performs during the state-space exploration.
They show substantial gain in space reduction without practical loss
in the capability of finding errors.  We plan to evaluate \tname{}
with CHESS-like search in the future.}
%\vspace{1ex}
\noindent\textbf{Model checking.}~ A
software model checker takes as input a test driver and explores the state-space
of a program, reachable from the test driver, in seek of errors like races and
deadlocks [13, 24, 22]. The approach is sound (i.e., it reports no false positives),
however, the exploration of large state-spaces can be very expensive. In this context,
time efficiency becomes an important requirement: the errors that a model checker
can find are subject to one manually-written test driver and the runtime cost
associated with the exploration of the state-space from that test driver often can
be very high.
Heuristic model checking
has been investigated under different contexts in the
past~\citep{groce02:model,rungta-mercer-haifa2008}. Rungta and
Mercer~\citep{rungta-mercer-haifa2008}, for example, use the warnings
produced by tools such as FindBugs~\citep{findbugs-web-page} or
JLint~\citep{jlint-web-page} to drive state-space exploration. \comment{ One
important difference to our approach is that we do not try to severely
constrain the search space as that could prevent the search from
exploring necessary states to provoke race.  More precisely, our
heuristic only increases the priority of selected threads for the
purpose of scheduling as opposed to guiding the search towards
specific program statements.}

\Comment{ Even though it is possible to build on similar ideas to
  guide exploration with the output of \tname{}, this is orthogonal to
  our current goal.  Note that the use of \tname{} does \emph{not}
  interfere in search order and the capability of the model checker in
  finding different kinds of errors.}

%\vspace{1ex}
\noindent\textbf{Predictive analysis.}~Predictive analysis
has gained force recently as a dynamic technique to find concurrency
errors~\citep{feng-chen-2008,sorrentino-fse2010,ganai-ase2011,huang-zhang-issta2011}.
The typical approach uses a representative schedule of the program
(containing, for instance, reads and writes to memory, lock acquires
and releases, etc.) and, from that, infers new schedules based on some
criteria.  Different techniques vary in what they use to infer new
schedules (e.g., causal dependencies).  Considering that not all of
the schedules inferred are feasible in the program, some techniques,
like Penelope~\citep{sorrentino-fse2010}, execute the schedule to
confirm (or not) the fault.  The analysis involves the construction of
a model to represent the space of possible schedules, the analysis of
that model to produce schedules some of which may not be feasible, the
instrumentation of the program to make execution follow a particular
schedule, and the execution of inferred schedules. \comment{ In contrast to
predictive analysis tools that produce and execute different thread
schedules from some approximate model, our approach observes the
feasible schedules that a model checker explores so as to infer potential
races.  Our approach is orthogonal to existing predictive analysis
tools (even though it was inspired by them) and complementary to
stateful model checking.}

%\vspace{1ex}
\noindent\textbf{Static tools.}~Several static and dynamic
race detection tools have been previously proposed.  Static tools,
such as RacerX~\citep{engler-ashcraft-2003} and
Chord~\citep{naik-etal-pldi2006}, are typically fast but can report
many false alarms due the conservative assumptions that accumulate
during the analysis.  Static tools based on pattern matching such as
FindBugs~\citep{findbugs-web-page} or JLint~\citep{jlint-web-page} can
in addition miss errors due to an incomplete set of supported
patterns.  Compared to static tools, dynamic based analisys are often more precises and reportes less falses positives, however static tools \comment{the warnings \tname{} reports are
based on dynamic information and therefore do not suffer from the same
sources of imprecision.  Our approach is complementary to static
tools; it builds on model checkers that require different inputs and
provide different guarantees.}

%% information of
%% multiple execution traces across state-space exploration and it
%% non-intrusively integrates with model checkers.

\Comment{
This allows the model checker to find other kinds of errors like
assertion violations or deadlocks in case the application does not
contain races.}

%%\section{Model checking vs. Predictive Analysis}

%% \textbf{Software model checking vs. Predictive Analysis.}  It is very
%% important to stress that our goal is to report likely data-race
%% warnings during software model checking under the assumption that
%% finding actual errors can be very time consuming.  Our approach to
%% report warnings of race is subject to different requirements compared
%% to predictive analysis tools such as BIST~\cite{?},
%% Penelope~\cite{sorrentino-fse2010} and
%% JPredictor~\cite{feng-chen-2008} (see Section~\ref{sec:related}).  In
%% particular, we do not want to significantly affect state-space
%% exploration time.

%% \Comment{
%% still want to perform model-checking so to find actual
%% errors.  Given that, we do not want to significantly affect model
%% checking performance.}

%% \Comment{
%% To the best of our knowledge, this is the first initiative to combine
%% predictive analysis and program model checking and doing so we
%% introduce a new dimension for predictive analysis: multiple traces.


%% Similarly to predictive analysis tools like ,
%% \tname{} speculates about alternative thread schedules.  In contrast,
%% it correlates coverage data information obtained across the
%% state-space exploration to infer likely races.  Existing predictive
%% algorithms consider only one execution trace and applies more
%% expensive analysis based on that trace.  \Fix{explain this better}
%% }


%\vspace{1ex}
\comment{\noindent\textbf{Language support.}~To facilitate
development of multithreaded software, new methods~\citep{yi-ppopp2011}
and language support~\citep{Burckhardt:2010:CPR} have been
recently proposed and old languages regained
force~\citep{lauterburg-etal-ase09}.  The approach of \tname{}
complements these initiatives which aim at making concurrent software
safer.  It focuses on improving the support to the dominant model of
concurrent programming to date, which is based on the shared-memory
model.}

%% which often report higher ratios of false
%% alarms~\cite{luo-etal-scam2010}.


%% Dynamic
%% tools\Comment{~\cite{godefroid97:model,musuvathi02:cmc,visser03model,marino-etal-pldi2009,flanagan-freund-pldi2009}}
%% can be significantly slower compared to static tools and also miss
%% errors, however, they typically don't report false alarms.  


%% \Fix{Discuss high and low-level race detection.}

%% \Fix{revise this...}


%% Recently, Marino~\etal{}~\cite{marino-etal-pldi2009} realized that
%% sampling could be very helpful to speed-up detection of data-races.
%% They selectively monitor thread accesses based on data obtained with
%% profiling.  Even though their goal is different, their fundamental
%% idea is similar to ours.  They recognize that not all points of
%% execution deserve same attention.  



%% Previous dynamic analysis work focused on reducing cost of
%% instrumentation for efficient runtime
%% verification~\cite{schonberg-pldi1989,praun-gross-oopsla2001,pozniansky-schuster-2007,flanagan-freund-pldi2009,marino-etal-pldi2009},
%% and on improving precision of monitors~\cite{bodden-havelund-issta08}
%% that typically use variations of the Eraser lockset
%% algorithm~\cite{savage-etal-1997}.  These algorithms typically build
%% state machines too encode program states.  We remain to evaluate
%% whether \tname{} can leverage the distance to race states on these
%% state machines to adjust its measure of fitness.

%% \Fix{...Beverly Sanders work...}

%% \Fix{discuss race prediction analysis}

% LocalWords:  dataflow FindBugs JLint lossy Musuvathi Qadeer Rungta etal haifa
% LocalWords:  interleavings multithreaded chen fse ganai ase huang zhang issta
% LocalWords:  stateful RacerX ashcraft pldi BIST JPredictor ppopp flanagan
% LocalWords:  freund praun oopsla
